\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $x$:Id, $T$:Type, ${\it ks}$:Knd List,\+
\\[0ex]${\it tr}$:($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$) \}$\rightarrow$State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$$T$$\rightarrow$$T$).
\-\\[0ex]${\it ds}$ $\parallel$ $x$ : $T$ $\Rightarrow$ ($\forall$$k$:Knd. $k$ $\in$ dom(R{-}da(R{-}state{-}var($i$;${\it ds}$;${\it da}$;$x$;$T$;${\it ks}$;${\it tr}$);$i$)) $\Rightarrow$ ($k$ $\in$ ${\it ks}$))
\end{tabbing}